ecl-es-halt(es; x)
== ecl_ind(x;
== ecl_ind(k,test.(n,e1,e2. if (n = 0)
== ecl_ind(then e2 = 
== ecl_ind(then first e  e1.(es-kind(es; e) = k) c ((test(es-state-when(es; e),es-val(es; e))))
== ecl_ind(else False
== ecl_ind(fi );
== ecl_ind(a,b,ha,hb.(n,e1,e2. if (n = 0) then False else ha(n,e1,e2) fi 
== ecl_ind( e(e1,e2].(ha(0,e1,es-pred(es; e)))  (hb(n,e,e2)));
== ecl_ind(a,b,ha,hb.(n,e1,e2. if (n = 0)
== ecl_ind(then ((ha(0,e1,e2))  e[e1,e2].hb(0,e1,e))  ((hb(0,e1,e2))  e[e1,e2].ha(0,e1,e))
== ecl_ind(else ((ha(n,e1,e2))
== ecl_ind(else  l-all(cons(0; ecl-ex(b));
== ecl_ind(else  l-all(m.if n z m then e[e1,e2).(hb(m,e1,e)) else e[e1,e2].(hb(m,e1,e)) fi 
== ecl_ind(else  l-all())
== ecl_ind(else  ((hb(n,e1,e2))
== ecl_ind(else   l-all(cons(0; ecl-ex(a));
== ecl_ind(else   l-all(m.if n z m
== ecl_ind(else   l-all(then e[e1,e2).(ha(m,e1,e))
== ecl_ind(else   l-all(else e[e1,e2].(ha(m,e1,e))
== ecl_ind(else   l-all(fi ))
== ecl_ind(fi );
== ecl_ind(a,b,ha,hb.(n,e1,e2. ((ha(n,e1,e2))
== ecl_ind( l-all(cons(0; ecl-ex(b));
== ecl_ind( l-all(m.if n z m then e[e1,e2).(hb(m,e1,e)) else e[e1,e2].(hb(m,e1,e)) fi ))
== ecl_ind( ((hb(n,e1,e2))
== ecl_ind(  l-all(cons(0; ecl-ex(a));
== ecl_ind(  l-all(m.if n z m then e[e1,e2).(ha(m,e1,e)) else e[e1,e2].(ha(m,e1,e)) fi )));
== ecl_ind(a,ha.(n,e1,e2. if (n = 0)
== ecl_ind(then False
== ecl_ind(else [e1;e2]~([x,y].ha(0,x,y))*[x,y].ha(n,x,y)
== ecl_ind(fi );
== ecl_ind(a,m,ha.ha;
== ecl_ind(a,m,ha.(n,e1,e2. if (n = 0) then False else ha(n,e1,e2) fi 
== ecl_ind( if (n = m) then ha(0,e1,e2) else False fi );
== ecl_ind(a,l,ha.(n,e1,e2. ((ha(n,e1,e2))  ((n  l)))
== ecl_ind( if (n = 0) then l_exists(l; ; m.(ha(m,e1,e2))) else False fi )) 

latex

---

clarification:

ecl-es-halt(es; x)
== ecl_ind(x;
== ecl_ind(k,test.(n,e1,e2. if (n = 0)
== ecl_ind(then es-first-since(es;e.(es-kind(es; e) = k  Knd)
== ecl_ind(then c ((test(es-state-when(es; e),es-val(es; e))));e1;e2)
== ecl_ind(else False
== ecl_ind(fi );
== ecl_ind(a,b,ha,hb.(n,e1,e2. if (n = 0) then False else ha(n,e1,e2) fi 
== ecl_ind( existse-between3(es;e1;e2;e.(ha(0,e1,es-pred(es; e)))  (hb(n,e,e2))));
== ecl_ind(a,b,ha,hb.(n,e1,e2. if (n = 0)
== ecl_ind(then ((ha(0,e1,e2))  existse-between2(es;e1;e2;e.hb(0,e1,e)))
== ecl_ind(then  ((hb(0,e1,e2))  existse-between2(es;e1;e2;e.ha(0,e1,e)))
== ecl_ind(else ((ha(n,e1,e2))
== ecl_ind(else  l-all(cons(0; ecl-ex(b));
== ecl_ind(else  l-all(m.if n z m
== ecl_ind(else  l-all(then alle from es in [e1;e2).(hb(m,e1,e))
== ecl_ind(else  l-all(else alle-between2(es;e1;e2;e.(hb(m,e1,e)))
== ecl_ind(else  l-all(fi ))
== ecl_ind(else  ((hb(n,e1,e2))
== ecl_ind(else   l-all(cons(0; ecl-ex(a));
== ecl_ind(else   l-all(m.if n z m
== ecl_ind(else   l-all(then alle from es in [e1;e2).(ha(m,e1,e))
== ecl_ind(else   l-all(else alle-between2(es;e1;e2;e.(ha(m,e1,e)))
== ecl_ind(else   l-all(fi ))
== ecl_ind(fi );
== ecl_ind(a,b,ha,hb.(n,e1,e2. ((ha(n,e1,e2))
== ecl_ind( l-all(cons(0; ecl-ex(b));
== ecl_ind( l-all(m.if n z m
== ecl_ind( l-all(then alle from es in [e1;e2).(hb(m,e1,e))
== ecl_ind( l-all(else alle-between2(es;e1;e2;e.(hb(m,e1,e)))
== ecl_ind( l-all(fi ))
== ecl_ind( ((hb(n,e1,e2))
== ecl_ind(  l-all(cons(0; ecl-ex(a));
== ecl_ind(  l-all(m.if n z m
== ecl_ind(  l-all(then alle from es in [e1;e2).(ha(m,e1,e))
== ecl_ind(  l-all(else alle-between2(es;e1;e2;e.(ha(m,e1,e)))
== ecl_ind(  l-all(fi )));
== ecl_ind(a,ha.(n,e1,e2. if (n = 0)
== ecl_ind(then False
== ecl_ind(else es-pstar-q(es;x,y.ha(0,x,y);x,y.ha(n,x,y);e1;e2)
== ecl_ind(fi );
== ecl_ind(a,m,ha.ha;
== ecl_ind(a,m,ha.(n,e1,e2. if (n = 0) then False else ha(n,e1,e2) fi 
== ecl_ind( if (n = m) then ha(0,e1,e2) else False fi );
== ecl_ind(a,l,ha.(n,e1,e2. ((ha(n,e1,e2))  ((n  l  )))
== ecl_ind( if (n = 0) then l_exists(l; ; m.(ha(m,e1,e2))) else False fi )) 

latex

Definitions	False, f(a), , l_exists(L; T; x.P(x)), #$n, (i = j), if b then t else f fi , (x  l), A, P  Q, P  Q, x.A(x), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), e[e1,e2].P(e), e[e1,e2).P(e), i z j, ecl-ex(x), cons(car; cdr), l-all(L; x.P(x)), e[e1,e2].P(e), es-pred(es; e), e(e1,e2].P(e), es-val(es; e), es-state-when(es; e), b, es-kind(es; e), Knd, s = t, A c B, e2 = first e  e1.P(e), ecl ind
FDL editor aliases	ecl-es-halt